Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    primes  → sieve(from(s(s(0))))
2:    from(X)  → cons(X,n__from(n__s(X)))
3:    head(cons(X,Y))  → X
4:    tail(cons(X,Y))  → activate(Y)
5:    if(true,X,Y)  → activate(X)
6:    if(false,X,Y)  → activate(Y)
7:    filter(s(s(X)),cons(Y,Z))  → if(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y))))
8:    sieve(cons(X,Y))  → cons(X,n__filter(X,n__sieve(activate(Y))))
9:    from(X)  → n__from(X)
10:    s(X)  → n__s(X)
11:    filter(X1,X2)  → n__filter(X1,X2)
12:    cons(X1,X2)  → n__cons(X1,X2)
13:    sieve(X)  → n__sieve(X)
14:    activate(n__from(X))  → from(activate(X))
15:    activate(n__s(X))  → s(activate(X))
16:    activate(n__filter(X1,X2))  → filter(activate(X1),activate(X2))
17:    activate(n__cons(X1,X2))  → cons(activate(X1),X2)
18:    activate(n__sieve(X))  → sieve(activate(X))
19:    activate(X)  → X
There are 23 dependency pairs:
20:    PRIMES  → SIEVE(from(s(s(0))))
21:    PRIMES  → FROM(s(s(0)))
22:    PRIMES  → S(s(0))
23:    PRIMES  → S(0)
24:    FROM(X)  → CONS(X,n__from(n__s(X)))
25:    TAIL(cons(X,Y))  → ACTIVATE(Y)
26:    IF(true,X,Y)  → ACTIVATE(X)
27:    IF(false,X,Y)  → ACTIVATE(Y)
28:    FILTER(s(s(X)),cons(Y,Z))  → IF(divides(s(s(X)),Y),n__filter(n__s(n__s(X)),activate(Z)),n__cons(Y,n__filter(X,n__sieve(Y))))
29:    FILTER(s(s(X)),cons(Y,Z))  → ACTIVATE(Z)
30:    SIEVE(cons(X,Y))  → CONS(X,n__filter(X,n__sieve(activate(Y))))
31:    SIEVE(cons(X,Y))  → ACTIVATE(Y)
32:    ACTIVATE(n__from(X))  → FROM(activate(X))
33:    ACTIVATE(n__from(X))  → ACTIVATE(X)
34:    ACTIVATE(n__s(X))  → S(activate(X))
35:    ACTIVATE(n__s(X))  → ACTIVATE(X)
36:    ACTIVATE(n__filter(X1,X2))  → FILTER(activate(X1),activate(X2))
37:    ACTIVATE(n__filter(X1,X2))  → ACTIVATE(X1)
38:    ACTIVATE(n__filter(X1,X2))  → ACTIVATE(X2)
39:    ACTIVATE(n__cons(X1,X2))  → CONS(activate(X1),X2)
40:    ACTIVATE(n__cons(X1,X2))  → ACTIVATE(X1)
41:    ACTIVATE(n__sieve(X))  → SIEVE(activate(X))
42:    ACTIVATE(n__sieve(X))  → ACTIVATE(X)
The approximated dependency graph contains one SCC: {29,31,33,35-38,40-42}.
Tyrolean Termination Tool  (219.51 seconds)   ---  May 3, 2006